
We now state some properties of \rnd networks. 
The first property regards the number of tokens per place. By construction, we can show that at every instant each place of a \rnd network contains one and only one token. 
\begin{theorem}\label{th:safe}
Given a \rnd network $(\res, \RS)$:
\begin{enumerate}
 \item the initial marking $M_0$ contains exactly one token per place.  
 \item each reachable marking $M$ contains exactly one token per place. 
\end{enumerate}
\end{theorem}
\begin{proof}[Sketch]
Assume a \rnd network $(\res, \RS)$, we prove   each item.
\begin{enumerate}
 \item The proof follows from the observation that, by construction, the initial marking $M_0$ contains exactly one token per place (Definition \ref{def:rs}).

\item The proof follows by induction on the length of the firing sequence. Let $M$ be a reachable marking with corresponding  firing sequence $(t_1, \sigma_1), \dots, (t_n, \sigma_n)$.
\begin{itemize}
 \item {\bf Base case:} follows from item (1) above. 
 \item {\bf Inductive step:} let $\firing{M_{n-1}}{t_n}{\sigma_n}{M}$ be the last step of the firing sequence. By inductive hypothesis we know that $M_{n-1}$ is a marking that contains exactly one token per place. 
 Now, observe that for each type of transition ($t_n = t_c$ or $t_n = t_\rho$ for some $\rho \in \RS$) all adjacent places are simultaneously  input and output places: in some cases the token is just read (e.g.  for $t_\rho$ this is the case of reactants and inhibitors) in others it is replaced with a new one (e.g.  for $t_\rho$ this is the case for the place $q_{\rho}$ or the products). Hence, the new marking $M$ contains exactly one token per place, thus concluding the proof. \qed
\end{itemize}
 \end{enumerate}
\end{proof}

% The second theorem states that the construction of a \rnd network is sound and complies with the Assumptions in section \ref{sec:reaction}.
% 
% \begin{theorem}\label{lem:m0}
%  Every \rnd network \rndnet satisfies Assumptions 1--6.
% \end{theorem}
% \begin{proof}
% We analyze each Assumption separately:
% \begin{enumerate}[{A}1)]
%  \item It follows from the fact that \rndnet  contains a single clock represented by $\Pclock$ and that all other transitions are connected to it.
%  \item It follows from the definition of initial marking in Definition \ref{def:rs}.
%  \item It follows from the fact that all species are linked to transition $t_c$ that is responsible of updating the clock.
% More precisely, each guard $C_s$ performs a check on the actual state of species $s$ and dependently on the age of the species decides whether it has to decay or not.  
% \item It follows from Assumptions (A\ref{item:global}), (A\ref{item:init}), (A\ref{item:clock}) and (A\ref{item:augred}).
% \item The assumption can be found in the label  $L(t_{\rho})$ of transitions corresponding to reactions.
% \item This is precisely the content of guards $C_{p+}$ and $C_{p-}$.
% %\item 
% 
% \end{enumerate}
% This concludes the proof.  \qed
% \end{proof}

Observe that, during a reaction, each product $p$ can only be increased or decreased by at most one level. Similarly, decay can only decrease the level of a species $s$ by at most one. As a consequence,   tuple $\birth_s$ in place $q_s$ has a special invariant form detailed in the theorem below. 

\begin{theorem}
Given a \rnd network $(\res, \RS)$, for each place $q_s$ ($ \forall s \in \res$) and for every reachable marking $M$ such that 
$M(q_s)= \tuple{\lev_s, \refr_s, \birth_s}$ we have the following invariant: 
$$ \forall k \in [0..\lev_s], \ \birth_s[k]\leq\birth_s[k+1]  \text{ and } 
\forall  k \in [\lev_s+1..\setlev_s-1], \ \birth_s[k]\geq\birth_s[k+1] $$
\end{theorem}
\begin{proof}[Sketch]
 The proof proceeds by induction on the length of the firing sequence $(t_1, \sigma_1), \dots, (t_n, \sigma_n)$ to reach marking $M$.
 
 \begin{itemize}
 \item {\bf Base case:} follows  from the definition of initial marking in Definition \ref{def:rs}.
 \item {\bf Inductive step:} let $\firing{M_{n-1}}{t_n}{\sigma_n}{M}$ be the last step of the firing sequence. By inductive hypothesis we know that $M_{n-1}$ is a marking where for each place $q_s$ ($ s \in \res$)$, M_{n-1}(q_s)= \tuple{\lev_s, \refr_s, \birth_s}$,  $ \forall k \in [0..\lev_s], \ \birth_s[k]\leq\birth_s[k+1]$  and $\forall  k \in [\lev_s+1..\setlev_s-1], \ \birth_s[k]\geq\birth_s[k+1] $. We now proceed by case analysis on the type of transition $t_n$.
 \begin{description}
  \item[$t_n = t_c$: ] $t_n$ is the clock transition. Suppose $z$ is the value of the clock. Depending on the value of $z-\refr_s$ the token in $q_s$ either remains unchanged or it is updated to $\tuple{\lev_s-1, z+1, \birth_s\sub{z+1}{\lev_s}}$. Now by inductive hypothesis we have that  $\forall k \in [0..\lev_s-1], \ \birth_s[k]\leq\birth_s[k+1]$ and $\forall  k \in [\lev_s+1..\setlev_s-1], \ \birth_s[k]\geq\birth_s[k+1]$. Moreover as $\birth_s[\lev_s]$ is updated to $z+1$ and as the values of the clock can only grow we also have that $\birth_s[\lev_s] \geq  \birth_s[\lev_s+1]$ thus concluding this case.
  \item [$t_n = t_{\rho}$: ]  $t_n$ is the transition corresponding to reaction $\rho$. Similarly as before, suppose $z$ is the value of the clock. If $s$ is a reactant or an inhibitor the token in $q_s$ remains unchanged. Otherwise $s$ is  a product and its  level can be either incremented or decremented. In the case it is incremented the token in $q_s$ is updated to  $\tuple{ \lev_s+1, z, \birth_s\sub{z}{\lev_s +1}}$.  By inductive hypothesis we have that  $\forall k \in [0..\lev_s], \ \birth_s[k]\leq\birth_s[k+1]$ and $\forall  k \in [\lev_s+2..\setlev_s-1], \ \birth_s[k]\geq\birth_s[k+1]$. Moreover as $\birth_s[\lev_s+1]$ is updated to $z$ and as the values of the clock can only grow we also have that $\birth_s[\lev_s] \leq  \birth_s[\lev_s+1]$. In the case species $s$ is decremented the token in $q_s$ is updated to  $\tuple{ \lev_s-1, z, \birth_s\sub{z}{\lev_s}}$.  By inductive hypothesis we have that  $\forall k \in [0..\lev_s-1], \ \birth_s[k]\leq\birth_s[k+1]$ and $\forall  k \in [\lev_s+1..\setlev_s-1], \ \birth_s[k]\geq\birth_s[k+1]$. Moreover as $\birth_s[\lev_s]$ is updated to $z$ and as the values of the clock can only grow we also have that $\birth_s[\lev_s] \geq  \birth_s[\lev_s+1]$ thus concluding this case and the proof of the theorem. \qed
 \end{description}
 \end{itemize}
\end{proof}